Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(h,z),app(e,x))  → app(app(h,app(c,z)),app(app(d,z),x))
2:    app(app(d,z),app(app(g,0),0))  → app(e,0)
3:    app(app(d,z),app(app(g,x),y))  → app(app(g,app(e,x)),app(app(d,z),y))
4:    app(app(d,app(c,z)),app(app(g,app(app(g,x),y)),0))  → app(app(g,app(app(d,app(c,z)),app(app(g,x),y))),app(app(d,z),app(app(g,x),y)))
5:    app(app(g,app(e,x)),app(e,y))  → app(e,app(app(g,x),y))
There are 18 dependency pairs:
6:    APP(app(h,z),app(e,x))  → APP(app(h,app(c,z)),app(app(d,z),x))
7:    APP(app(h,z),app(e,x))  → APP(h,app(c,z))
8:    APP(app(h,z),app(e,x))  → APP(c,z)
9:    APP(app(h,z),app(e,x))  → APP(app(d,z),x)
10:    APP(app(h,z),app(e,x))  → APP(d,z)
11:    APP(app(d,z),app(app(g,0),0))  → APP(e,0)
12:    APP(app(d,z),app(app(g,x),y))  → APP(app(g,app(e,x)),app(app(d,z),y))
13:    APP(app(d,z),app(app(g,x),y))  → APP(g,app(e,x))
14:    APP(app(d,z),app(app(g,x),y))  → APP(e,x)
15:    APP(app(d,z),app(app(g,x),y))  → APP(app(d,z),y)
16:    APP(app(d,app(c,z)),app(app(g,app(app(g,x),y)),0))  → APP(app(g,app(app(d,app(c,z)),app(app(g,x),y))),app(app(d,z),app(app(g,x),y)))
17:    APP(app(d,app(c,z)),app(app(g,app(app(g,x),y)),0))  → APP(g,app(app(d,app(c,z)),app(app(g,x),y)))
18:    APP(app(d,app(c,z)),app(app(g,app(app(g,x),y)),0))  → APP(app(d,app(c,z)),app(app(g,x),y))
19:    APP(app(d,app(c,z)),app(app(g,app(app(g,x),y)),0))  → APP(app(d,z),app(app(g,x),y))
20:    APP(app(d,app(c,z)),app(app(g,app(app(g,x),y)),0))  → APP(d,z)
21:    APP(app(g,app(e,x)),app(e,y))  → APP(e,app(app(g,x),y))
22:    APP(app(g,app(e,x)),app(e,y))  → APP(app(g,x),y)
23:    APP(app(g,app(e,x)),app(e,y))  → APP(g,x)
The approximated dependency graph contains one SCC: {6,9,12,15,16,18,19,22}.
Tyrolean Termination Tool  (0.58 seconds)   ---  May 3, 2006